package list;

import java.io.Serializable;
import java.util.LinkedList;

import randoop.CheckRep;

import korat.finitization.IClassDomain;
import korat.finitization.IFinitization;
import korat.finitization.IIntSet;
import korat.finitization.IObjSet;
import korat.finitization.impl.FinitizationFactory;



/**
 * Implementacion del TAD Lista, usando una estructura dinámica, más 
 * precisamente un árbol binario de búsqueda.
 * Esta clase implementa los métodos abstractos declarados en List, y
 * corresponde a una implementación polimórfica.
 * @author Nazareno Aguirre, Valeria Bengolea & Renzo Degiovanni
 * @version 0.1 22/04/2013
 */
public class TreeList implements List, Serializable{
	
    /**
	 * 
	 */
	private static final long serialVersionUID = 407102241690509045L;

	private Node root; // tree that stores list' elements

    private int size; // number of elements in the list
    
    private int lastIndex = -1; //used by repOKp

    public TreeList(){}

	public boolean isEmpty() {
		return size == 0;
	}
	
	public int size() {
		return size;
	}
	
	/*--------------------------------------------------------------------*/
    /* removeAll(): removes all the items from the list                   */
    /* Precondition: None                                                 */
    /* Postcondition: all elements are removed from the list.             */
    /*--------------------------------------------------------------------*/	
	public void removeAll() {
		root = null;
		size = 0;
	}
	
	/*--------------------------------------------------------------------*/
    /* add(int index, Object item ): adds item to the list in position    */
    /*                               index                                */
    /*--------------------------------------------------------------------*/	
	public void add(int index, Object item) throws RuntimeException, IndexOutOfBoundsException {
		if (item == null) throw new RuntimeException("attempting to insert null object");
		if (index<0 || index>size) throw new IndexOutOfBoundsException("index out of bounds in tree list");
		//TODO: Partially implemented routine;
		//IMPLEMENTATION
		Node newNode = new Node(null, null, index, item);
		root = addNode(root, newNode);
		this.size++;
	}
	
	private Node addNode(Node root, Node newNode) {
		if (root == null) {
			return newNode;
		} else {
			int index = newNode.getIndex();
			if (index < root.getIndex()) {
				root.setLeft(addNode(root.getLeft(), newNode));
				root.setIndex(root.getIndex()+1);
				updateIndex(root.getRight(), true);
			} else if (index > root.getIndex()) {
				root.setRight(addNode(root.getRight(), newNode));
			} else {
				root.setIndex(root.getIndex()+1);
				updateIndex(root.getRight(), true);
				if (index < root.getIndex()) {
					root.setLeft(addNode(root.getLeft(), newNode));
				} else {
					root.setRight(addNode(root.getRight(), newNode));
				}
			}
			return root;
		}
	}
	
	private void updateIndex(Node n, boolean mod) {
		int change = mod?1:-1;
		if (n == null) return;
		n.setIndex(n.getIndex()+change);
		updateIndex(n.getLeft(), mod);
		updateIndex(n.getRight(), mod);
	}
	
	
	/*--------------------------------------------------------------------*/
    /* remove(int index): removes item in the index position of the list  */
    /*--------------------------------------------------------------------*/	
	public void remove(int index) throws IndexOutOfBoundsException {
		if(root != null){
			if (index<0 || index>=size) throw new IndexOutOfBoundsException("index out of bounds in tree list");
				
			root = removeNode(root, index);
			size--;
		}
	}
	
	private Node removeNode(Node e, int index) {
		if(e.isLeaf() && index == e.getIndex()){
			return null;
		}else{
			if(index < e.getIndex()){
				e.setIndex(e.getIndex()-1);
				e.setLeft(removeNode(e.getLeft(), index));
				updateIndex(e.getRight(), false);
			}else if(index > e.getIndex()){
				e.setRight(removeNode(e.getRight(), index));
			}
			else{
				if(e.getLeft() != null && e.getRight() != null){
					updateIndex(e.getRight(), false);
					if (e.getLeft().isLeaf()) {
						e.getLeft().setRight(e.getRight());
					} else {
						Node father = getFatherNode(e.getLeft(), index-1);
						updateIndex(father.getRight(), false);
						e.setIndex(father.getRight().getIndex());
						e.setInfo(father.getRight().getInfo());
						father.setRight(father.getRight().getLeft());
					}
					return e;
				}else{
					if(e.getLeft() == null){
						updateIndex(e.getRight(), false);
						return e.getRight();
					}else{ 
						return e.getLeft();
					}
				}
			}
		}
		return e;
	}
	

	
	/*--------------------------------------------------------------------*/
    /* get(int index): returns the reference to the object in position    */
    /*                 index                                              */
    /*--------------------------------------------------------------------*/	
	public Object get(int index) throws IndexOutOfBoundsException {
		if (index<0 || index>=size) throw new IndexOutOfBoundsException("index out of bounds in tree list");
		//TODO: Partially implemented routine;
		//IMPLEMENTATION
		Node res = getNode(this.root, index);
		if (res != null) {
			return res.getInfo();
		} else {
			return null;
		}
	}
	
	private Node getNode(Node e, int index) {
		if (e == null) {
			return null;
		} else {
			if (index < e.getIndex()) {
				return getNode(e.getLeft(), index);
			} else if (index > e.getIndex()) {
				return getNode(e.getRight(), index);
			} else {
				return e;
			}
		}
	}

	
	private Node getFatherNode(Node e, int index) {
		if (e == null) {
			return null;
		} else {
			if(e.getLeft().getIndex() == index || e.getRight().getIndex() == index ){
				return e;
			}
			if (index < e.getIndex()) {
				return getFatherNode(e.getLeft(), index);
			} else{
				return getFatherNode(e.getRight(), index);
			}
		}
	}
	
	/** 
	 * invariante de representación de la estructura.
	 * @return true si y sólo si la estructura es internamente consistente
	 * @pre. true  
	 * @post. Se retorna true si y sólo si root aloja un árbol binario de búsqueda (respecto a index),
	 * todos los elementos del árbol son no nulos (respecto a info), size se corresponde con el número de nodos del 
	 * árbol, y las claves del árbol son 0..size-1.	 
	 */				
	@CheckRep
	public boolean repOK() { 		
		java.util.List/*<Node>*/ visited = new LinkedList/*<Node>*/();
		this.lastIndex = -1;
		if (root == null) {
			return this.size == 0;
		}
		if (root.getInfo() == null) {
			return false;
		}
		if (!(root.getIndex() >= 0 && root.getIndex() < this.size)) {
			return false;
		}
		visited.add(root);
		if (root.getLeft() == null) this.lastIndex = root.getIndex();
		int leftSize;
		leftSize = repOKp(root.getLeft(), visited, 0);
		if (leftSize == -1) {
			return false;
		}
		if (this.root.getLeft() != null && this.lastIndex != root.getIndex()-1) return false;
		this.lastIndex = root.getIndex();
		if (repOKp(root.getRight(), visited, leftSize+1) == -1) return false; 
		return visited.size() == size;
	}
	
	private int repOKp(Node e, java.util.List/*<Node>*/ visited, int index) {
		int leftSize, rightSize;
		if (e == null) {
			return 0;
		}
		if (e.getInfo() == null) {
			return -1;
		}
		if (e.getIndex() < 0 || e.getIndex() >= this.size) {
			return -1;
		}
		if (visited.contains(e)) {
			return -1;
		}
		visited.add(index, e);
		if (visited.size() > size) {
			return -1;
		}
		boolean skip = false;
		if (this.lastIndex == -1 && e.getLeft() == null) {
			this.lastIndex = e.getIndex();
			skip = true;
		}
		
		leftSize = repOKp(e.getLeft(), visited, index);
		if (leftSize == -1) {
			return -1;
		}
		if (!skip && this.lastIndex != e.getIndex()-1) return -1;
		this.lastIndex = e.getIndex();
		
		rightSize = repOKp(e.getRight(), visited, leftSize+index+1);
		
		if (rightSize == -1) {
			return -1;
		}
		
		return 1+rightSize+leftSize;
	}


    public String toString() {
        StringBuffer buf = new StringBuffer();
        buf.append("{");
        if (root != null)
            buf.append(root.toString());
        buf.append("}");
        return buf.toString();
    }
    
    @Override
    public TreeList clone() {
    	TreeList newList = new TreeList();
    	newList.size = this.size;
    	newList.root = this.root==null?null:this.root.clone();
    	return newList;
    }
    
    
    public static IFinitization finTreeList(int nodesN, int minSize, int maxSize, int minIndex, int maxIndex, int minInfo, int maxInfo) {
    	IFinitization f = FinitizationFactory.create(TreeList.class);
    	IObjSet nodes = f.createObjSet(Node.class, nodesN, true);
    	IIntSet indices = f.createIntSet(minIndex, maxIndex);
    	IObjSet elems = f.createObjSet(Integer.class);
    	IClassDomain elemsClassDomain = f.createClassDomain(Integer.class);
    	elemsClassDomain.includeInIsomorphismCheck(false);
    	for (int i = minInfo; i <= maxInfo; i++)
    	elemsClassDomain.addObject(new Integer(i));
    	elems.addClassDomain(elemsClassDomain);
    	f.set("root", nodes);
    	f.set("Node.left", nodes);
    	f.set("Node.right", nodes);
    	f.set("Node.index", indices);
    	f.set("Node.info", elems);
    	IIntSet sizes = f.createIntSet(minSize, maxSize);
    	f.set("size", sizes);
    	return f;
    }
    
    public static IFinitization finTreeList(int nodesN, int minSize, int maxSize, int minIndex, int maxIndex) {
    	IFinitization f = FinitizationFactory.create(TreeList.class);
    	IObjSet nodes = f.createObjSet(Node.class, nodesN, true);
    	IIntSet indices = f.createIntSet(minIndex, maxIndex);
    	IObjSet elems = f.createObjSet(Integer.class);
    	IClassDomain elemsClassDomain = f.createClassDomain(Integer.class);
    	elemsClassDomain.includeInIsomorphismCheck(false);
    	for (int i = minIndex; i <= maxIndex; i++)
    	elemsClassDomain.addObject(new Integer(i));
    	elems.addClassDomain(elemsClassDomain);
    	f.set("root", nodes);
    	f.set("Node.left", nodes);
    	f.set("Node.right", nodes);
    	f.set("Node.index", indices);
    	f.set("Node.info", elems);
    	IIntSet sizes = f.createIntSet(minSize, maxSize);
    	f.set("size", sizes);
    	return f;
    }
    
    public static IFinitization finTreeList(int nodesN, int minSize, int maxSize) {
    	return finTreeList(nodesN, minSize, maxSize, minSize, maxSize);
    }
    
    public static IFinitization finTreeList(int nodesN) {
    	return finTreeList(nodesN, 0, nodesN);
    }
	

}
